A:Type, B:(AType), eq:EqDecider(A), f, g:a:A fp B(a). f  g  f || g 

latex

Definitions	f  g, f || g, P & Q, Prop, b, x  dom(f), f(x), Top, a:A fp B(a), x. t(x), x(s), EqDecider(T), t  T, x:A. B(x), P  Q, A & B
Lemmas	deq wf, fpf wf, fpf-trivial-subtype-top, fpf-ap wf, fpf-dom wf, assert wf